package kodkod.analysis;

import kodkod.analysis.ast.ExtendedVoidVisitor;

import java.util.*;

import kodkod.ast.*;
import kodkod.ast.operator.FormulaOperator;
import kodkod.ast.operator.Quantifier;

public class OverallAnalysis extends ExtendedVoidVisitor {
	
	public HashMap<Relation, LeafInfo> leafInfos;
	
	public HashMap<Variable, Expression> decls;
	public HashMap<Variable, Expression> allDecls;
	
	public ArrayList<IfExpression> ifExpressions = new ArrayList<IfExpression>();
	public ArrayList<IfIntExpression> ifIntExpressions = new ArrayList<IfIntExpression>();
	public ArrayList<Comprehension> comprehensions = new ArrayList<Comprehension>();
	
	boolean negated = false;
		
	public OverallAnalysis(Formula formula) {
		leafInfos = new HashMap<Relation, LeafInfo>();
		
		decls = new HashMap<Variable, Expression>();
		allDecls = new HashMap<Variable, Expression>();
		
		this.visit(formula);
	}
	
	public boolean visited(Node node) {return false;}
		
	@Override
	public void visit(Relation relation) {
		if (Analyzer.translation.primaryRelations.contains(relation)) {
			int index = Analyzer.translation.primaryRelations.indexOf(relation);
			leafInfos.put(relation, new LeafInfo(relation, index));
		}
	}
	@Override
	public void visit(Variable variable) {
		if (Analyzer.translation.skolemRelations.containsKey(variable)) {
			Relation relation = Analyzer.translation.skolemRelations.get(variable);
			int index = Analyzer.translation.primaryRelations.indexOf(relation);
			leafInfos.put(relation, new LeafInfo(relation, index));
		}
	}
	
	@Override
	public void visit(Comprehension comprehension) {
		for (Decl decl : comprehension.decls()) {
			allDecls.put(decl.variable(), decl.expression());
			decls.put(decl.variable(), decl.expression());
		}
		
		super.visit(comprehension.formula());
		negated = !negated;
		super.visit(comprehension.formula());
		negated = !negated;
		
		comprehensions.add(comprehension);
	}
	
	public void visit(IfExpression ifExpr) {
		super.visit(ifExpr);
		negated = !negated;
		super.visit(ifExpr);
		negated = !negated;
		
		ifExpressions.add(ifExpr);
	}
	
	public void visit(IfIntExpression intExpr) {
		super.visit(intExpr);
		negated = !negated;
		super.visit(intExpr);
		negated = !negated;
		
		ifIntExpressions.add(intExpr);
	}

	@Override
	public void visit(QuantifiedFormula qFormula) {
		for (Decl decl : qFormula.decls()) {
			decls.put(decl.variable(), decl.expression());
			if (negated != qFormula.quantifier().equals(Quantifier.ALL)) allDecls.put(decl.variable(), decl.expression());
		}
		
		super.visit(qFormula);
	}

	@Override
	public void visit(BinaryFormula node) {
		if (node.op().equals(FormulaOperator.AND) || node.op().equals(FormulaOperator.OR)) {
			super.visit(node);
		} else if (node.op().equals(FormulaOperator.IMPLIES)) {
			negated = !negated;
			node.left().accept(this);
			negated = !negated;
			node.right().accept(this);
		} else {
			super.visit(node);
			negated = !negated;
			super.visit(node);
			negated = !negated;
		}
	}

	@Override
	public void visit(NotFormula not) {
		negated = !negated;
		super.visit(not);
		negated = !negated;
	}
}
